fib1(N) -> sel2(N, fib12(s1(0), s1(0)))
fib12(X, Y) -> cons2(X, fib12(Y, add2(X, Y)))
add2(0, X) -> X
add2(s1(X), Y) -> s1(add2(X, Y))
sel2(0, cons2(X, XS)) -> X
sel2(s1(N), cons2(X, XS)) -> sel2(N, XS)
↳ QTRS
↳ DependencyPairsProof
fib1(N) -> sel2(N, fib12(s1(0), s1(0)))
fib12(X, Y) -> cons2(X, fib12(Y, add2(X, Y)))
add2(0, X) -> X
add2(s1(X), Y) -> s1(add2(X, Y))
sel2(0, cons2(X, XS)) -> X
sel2(s1(N), cons2(X, XS)) -> sel2(N, XS)
FIB12(X, Y) -> ADD2(X, Y)
ADD2(s1(X), Y) -> ADD2(X, Y)
SEL2(s1(N), cons2(X, XS)) -> SEL2(N, XS)
FIB1(N) -> SEL2(N, fib12(s1(0), s1(0)))
FIB12(X, Y) -> FIB12(Y, add2(X, Y))
FIB1(N) -> FIB12(s1(0), s1(0))
fib1(N) -> sel2(N, fib12(s1(0), s1(0)))
fib12(X, Y) -> cons2(X, fib12(Y, add2(X, Y)))
add2(0, X) -> X
add2(s1(X), Y) -> s1(add2(X, Y))
sel2(0, cons2(X, XS)) -> X
sel2(s1(N), cons2(X, XS)) -> sel2(N, XS)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
FIB12(X, Y) -> ADD2(X, Y)
ADD2(s1(X), Y) -> ADD2(X, Y)
SEL2(s1(N), cons2(X, XS)) -> SEL2(N, XS)
FIB1(N) -> SEL2(N, fib12(s1(0), s1(0)))
FIB12(X, Y) -> FIB12(Y, add2(X, Y))
FIB1(N) -> FIB12(s1(0), s1(0))
fib1(N) -> sel2(N, fib12(s1(0), s1(0)))
fib12(X, Y) -> cons2(X, fib12(Y, add2(X, Y)))
add2(0, X) -> X
add2(s1(X), Y) -> s1(add2(X, Y))
sel2(0, cons2(X, XS)) -> X
sel2(s1(N), cons2(X, XS)) -> sel2(N, XS)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
SEL2(s1(N), cons2(X, XS)) -> SEL2(N, XS)
fib1(N) -> sel2(N, fib12(s1(0), s1(0)))
fib12(X, Y) -> cons2(X, fib12(Y, add2(X, Y)))
add2(0, X) -> X
add2(s1(X), Y) -> s1(add2(X, Y))
sel2(0, cons2(X, XS)) -> X
sel2(s1(N), cons2(X, XS)) -> sel2(N, XS)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
SEL2(s1(N), cons2(X, XS)) -> SEL2(N, XS)
POL(SEL2(x1, x2)) = 3·x1 + x1·x2 + 2·x2
POL(cons2(x1, x2)) = 2 + 2·x2
POL(s1(x1)) = 2 + 2·x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
fib1(N) -> sel2(N, fib12(s1(0), s1(0)))
fib12(X, Y) -> cons2(X, fib12(Y, add2(X, Y)))
add2(0, X) -> X
add2(s1(X), Y) -> s1(add2(X, Y))
sel2(0, cons2(X, XS)) -> X
sel2(s1(N), cons2(X, XS)) -> sel2(N, XS)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
ADD2(s1(X), Y) -> ADD2(X, Y)
fib1(N) -> sel2(N, fib12(s1(0), s1(0)))
fib12(X, Y) -> cons2(X, fib12(Y, add2(X, Y)))
add2(0, X) -> X
add2(s1(X), Y) -> s1(add2(X, Y))
sel2(0, cons2(X, XS)) -> X
sel2(s1(N), cons2(X, XS)) -> sel2(N, XS)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ADD2(s1(X), Y) -> ADD2(X, Y)
POL(ADD2(x1, x2)) = x1
POL(s1(x1)) = 1 + x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
fib1(N) -> sel2(N, fib12(s1(0), s1(0)))
fib12(X, Y) -> cons2(X, fib12(Y, add2(X, Y)))
add2(0, X) -> X
add2(s1(X), Y) -> s1(add2(X, Y))
sel2(0, cons2(X, XS)) -> X
sel2(s1(N), cons2(X, XS)) -> sel2(N, XS)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
FIB12(X, Y) -> FIB12(Y, add2(X, Y))
fib1(N) -> sel2(N, fib12(s1(0), s1(0)))
fib12(X, Y) -> cons2(X, fib12(Y, add2(X, Y)))
add2(0, X) -> X
add2(s1(X), Y) -> s1(add2(X, Y))
sel2(0, cons2(X, XS)) -> X
sel2(s1(N), cons2(X, XS)) -> sel2(N, XS)